(set-logic HO_ALL)
(set-info :status sat)
(define-fun plus ((x Int) (y Int)) Int (+ x y))
(declare-fun A () (Set Int))
(declare-fun sumPlus1 () Int)
(declare-fun sumPlus2 () Int)
(assert (= A (set.insert 1 2 (set.singleton 3))))
(assert (= sumPlus1 (set.fold plus 1 A)))
(assert (= sumPlus2 (set.fold plus 2 (as set.empty (Set Int)))))
(check-sat)
